es:event_system{i:l}, i:Id, P:({e:es-E(es)| loc(e) = i} prop{i:l}).
alle-at(es; i; e.P(e))  prop{i:l} 

latex

Definitions	x:A. B(x), prop{i:l}, t  T, alle-at(es; i; e.P(e)), x(s), P  Q
Lemmas	es-E wf, Id wf, es-loc wf, event system wf